\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$), $n$:$\mathbb{N}$,\+
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List), $k$:Knd, $s$:decl{-}state(${\it ds}$), $v$:ma{-}valtype(${\it da}$; $k$).
\-\\[0ex](ecl{-}trans{-}act(${\it ds}$; ${\it da}$; $A$)($n$,append($L$; cons($<$$k$, $s$, $v$$>$; []))))
\\[0ex]$\Leftarrow\!\Rightarrow$ (($k$ $\in$ ecl{-}trans{-}ks($A$)) c$\wedge$ ($\uparrow$(ecl{-}trans{-}a($A$)($n$,$k$,$s$,$v$,ecl{-}trans{-}state($A$; $L$)))))
\end{tabbing}